\begin{tabbing}
$\forall$${\it es}$:ES, ${\it ff}$:FIFO, ${\it f2f+}$:F2F+{-}decls.
\\[0ex]plus{-}ify\{i:l\}(${\it es}$;${\it ff}$;is\_req  ;is\_ack ;awaiting ;owes\_ack )
\\[0ex]$\Rightarrow$ \=($\forall$${\it sndr}$, ${\it rcvr}$:${\it ff}$.C, $e$, ${\it e'}$:E.\+
\\[0ex]([$e$: ${\it sndr}$ $--$is\_req  $\rightarrow$ ${\it rcvr}$] $\vee$ [$e$: ${\it rcvr}$ $--$is\_ack $\rightarrow$ ${\it sndr}$])
\\[0ex]$\Rightarrow$ ([${\it e'}$: ${\it sndr}$ $--$is\_req  $\rightarrow$ ${\it rcvr}$] $\vee$ [${\it e'}$: ${\it rcvr}$ $--$is\_ack $\rightarrow$ ${\it sndr}$])
\\[0ex]$\Rightarrow$ (${\it e'}$ $<$ $e$)
\\[0ex]$\Rightarrow$ ($\forall$$x$, ${\it x'}$:E. f2f+{-}pred($x$,$e$) $\Rightarrow$ f2f+{-}pred(${\it x'}$,${\it e'}$) $\Rightarrow$ (${\it x'}$ $<$ $x$)))
\-
\end{tabbing}